A:Type, eq1,eq2:EqDecider(A), f:fpf(A; a.top), x:A.
guard(((fpf-dom(eq2; x; f))  (fpf-dom(eq1; x; f)))) 

latex

Definitions	x:A. B(x), guard(T), P  Q, t  T, x. t(x), x(s), prop{i:l}
Lemmas	fpf-dom functionality, top wf, assert wf, fpf-dom wf, fpf wf, deq wf